『The Type Theory of Lean』

1. どんなもの？

2. 先行研究と比べてどこがすごい？

3. 技術や手法のキモはどこ？

4. どうやって有効だと検証した？

5. 議論はある？

6. 次に読むべき論文は？

table:単語

dependent type 依存型

subsingleton elimination 準単集合消去

propositional extensionality 命題的外延性

axiom of choice 選択公理

inaccessible cardinal 到達不能基数

Church-Rosser property Church-Rosser性

non-transitive 非推移的

undecidable 決定不可能

underapproximation 過小近似

normal form 正規形

typing 型付け

term 項

context 文脈

universe 宇宙

inductive type 帰納型

recursor 再帰子

constructor 構築子

predicate 述語

proof 証明

equality 等式？

bijection 全単射

sort function ソート関数

level expression レベル表現

universe variable 宇宙変数

well-typed 型付けされた

type preservation 型保存

translation rule 翻訳規則

eliminator 除去子

parametricity パラメトリシティ

small elimination 小除去

large elimination 大除去

ZFC translation ZFC翻訳

η rule イータ規則

β reduction ベータ簡約

κ reduction カッパ簡約

ι reduction イオタ簡約

ζ reduction ゼータ簡約

algorithmic equivalence アルゴリズム的同値

accumulator 累積変数

確認用

Q.